a:. ((a) ~ tt)  (a ~ ff) 

latex

ProofTree

Definitions	left + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), , s = t, b, A, b, x:A. B(x), , P  Q, t  T, s ~ t
Lemmas	bool wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert